Nuprl Lemma : R-plus_wf
11,40
postcript
pdf
A
,
B
:Realizer. R-plus(
A
;
B
)
Realizer
latex
Definitions
x
.
t
(
x
)
,
R-plus(
A
;
B
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
Lemmas
Rplus
wf
,
Rnone?
wf
,
ifthenelse
wf
,
es
realizer
wf
,
let
wf
origin
A, B:Realizer. R-plus(A;B) 
Realizer A, B:Realizer. R-plus(A;B) Realizer 
x. t(x) Tx:A. B(x)